14 Hard tautologies and optimal proof systems (BAPLaCT)